diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-02 16:34:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-02 16:55:16 +0200 |
| commit | 67500967edf584fcddc41c74aea09d48ee80a03c (patch) | |
| tree | a0c46b71ac7536317462836a1336f8d497ab553e /plugins/funind | |
| parent | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (diff) | |
Better struture for Ltac internalization environments in Constrintern.
Diffstat (limited to 'plugins/funind')
| -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 2ceda4f48..808b2604c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function let interp_casted_constr_with_implicits sigma env impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty,Id.Map.empty) c + ~allow_patvar:false c (* Construct a fixpoint as a Glob_term |