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 /plugins/ssrmatching | |
| 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 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index bf3e2ac1c..d4579c3a1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -838,7 +838,7 @@ let rec uniquize = function | Context.Rel.Declaration.LocalAssum _ as x -> x | Context.Rel.Declaration.LocalDef (x,_,y) -> Context.Rel.Declaration.LocalAssum(x,y) in - Environ.push_rel ctx_item env, h' + 1 in + EConstr.push_rel ctx_item env, h' + 1 in let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in let f = EConstr.of_constr f in let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in @@ -1091,7 +1091,7 @@ let thin id sigma goal = | None -> sigma | Some (hyps, concl) -> let sigma = !evdref in - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps (EConstr.of_constr concl) (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma |