diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 16:18:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
| tree | fc84ec244390beb2f495b024620af2e130ad5852 /tactics/inv.ml | |
| parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) | |
Definining EConstr-based contexts.
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 426749a75..ecb8eedac 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,10 +13,10 @@ open Names open Nameops open Term open Termops +open Environ open EConstr open Vars open Namegen -open Environ open Inductiveops open Printer open Retyping @@ -75,6 +75,7 @@ let make_inv_predicate env evd indf realargs id status concl = | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in + let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env !evd id concl) then @@ -132,6 +133,10 @@ let make_inv_predicate env evd indf realargs id status concl = build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in + let name_context env ctx = + let map f c = List.map (fun d -> Termops.map_rel_decl f d) c in + map EConstr.of_constr (name_context env (map EConstr.Unsafe.to_constr ctx)) + in let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to |