diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:08:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:13:22 +0100 |
| commit | 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch) | |
| tree | d70ab7e108af307cbd9e996b78e0f9f5e945aa42 /plugins/funind | |
| parent | fb59652405d0e6a9d1100142d473374cd82ae16b (diff) | |
Removing the need of evarmaps in constr internalization.
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dc59b7ca..661e5e486 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = - Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls + Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty) c (* diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b7c471f4a..ac54e44cc 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -71,7 +71,7 @@ let isVarf f x = let ident_global_exist id = try let ans = CRef (Libnames.Ident (Loc.ghost,id)) in - let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in + let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when Errors.noncritical e -> false |