diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-13 12:49:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-13 12:49:54 +0200 |
| commit | f3b84cf63c242623bdcccd30c536e55983971da5 (patch) | |
| tree | 740984c577ed75c76edc2525b3de9bf744da3c21 /plugins/firstorder | |
| parent | b68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff) | |
| parent | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (diff) | |
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contains evars
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 285991797..83fbc2d5d 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -77,14 +77,14 @@ module CM=Map.Make(Constr) module History=Set.Make(Hitem) let cm_add sigma typ nam cm= - let typ = EConstr.to_constr sigma typ in + let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in try let l=CM.find typ cm in CM.add typ (nam::l) cm with Not_found->CM.add typ [nam] cm let cm_remove sigma typ nam cm= - let typ = EConstr.to_constr sigma typ in + let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in try let l=CM.find typ cm in let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in @@ -152,7 +152,7 @@ let re_add_formula_list sigma lf seq= redexes=List.fold_right HP.add lf seq.redexes; context=List.fold_right do_one lf seq.context} -let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context) +let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context) (*let rev_left seq= try |