diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 15:39:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:33 +0100 |
| commit | 536026f3e20f761e8ef366ed732da7d3b626ac5e (patch) | |
| tree | 571e44e2277b6d045d6c11fafca58b5ea6e43afa /pretyping/constr_matching.ml | |
| parent | ca993b9e7765ac58f70740818758457c9367b0da (diff) | |
Cleaning up opening of the EConstr module in pretyping folder.
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ecf6b1121..4d2500ccd 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -238,7 +238,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels match EConstr.kind sigma c2 with | Proj (pr, c) when not (Projection.unfolded pr) -> (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in - sorec ctx env subst p (EConstr.of_constr term) + sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _ -> raise PatternMatchingFailure) @@ -254,7 +254,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels else raise PatternMatchingFailure | _, Proj (pr,c) when not (Projection.unfolded pr) -> (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in - sorec ctx env subst p (EConstr.of_constr term) + sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _, _ -> try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2 @@ -266,7 +266,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (c, args), Proj (pr, c2) -> (try let term = Retyping.expand_projection env sigma pr c2 [] in - sorec ctx env subst p (EConstr.of_constr term) + sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> @@ -460,7 +460,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = if partial_app then try let term = Retyping.expand_projection env sigma p c' [] in - aux env (EConstr.of_constr term) mk_ctx next + aux env term mk_ctx next with Retyping.RetypeError _ -> next () else try_aux [env, c'] next_mk_ctx next |