diff options
| author | Pierre-Marie Pédrot | 2013-12-17 15:08:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-17 15:13:22 +0100 |
| commit | 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch) | |
| tree | d70ab7e108af307cbd9e996b78e0f9f5e945aa42 /plugins/funind/indfun.ml | |
| 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/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dc59b7ca7..661e5e4869 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 (* |