wip safeguard

math-comp · Apr 20, 2021 · 36138cb · 36138cb
1 parent e4dc108
commit 36138cb
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/HB/structure.elpi b/HB/structure.elpi
@@ -580,7 +580,13 @@ mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "Type" ; get-option ID ""
 mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "_ -> _"), !,
   @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
   phant.fun-infer-type funclass {coq.id->name ID} Ty PhT R.
+mk-infer T (w-params.cons ID Ty W) R :- get-option ID "off", !,
+  @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
+  phant.fun-real {coq.id->name ID} Ty PhT R.
 mk-infer T (w-params.cons ID Ty W) R :- not (get-option ID _), !,
+  if (coq.safe-dest-app Ty (global GR) _, is-structure GR)
+     (coq.error "HB: parameter" ID "is a structure but no form of inference specified")
+     true,
   @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
   phant.fun-real {coq.id->name ID} Ty PhT R.
 mk-infer _ (w-params.cons ID _ _) _ :- get-option ID Infer,