diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 19:02:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:26 +0100 |
| commit | 85ab3e298aa1d7333787c1fa44d25df189ac255c (patch) | |
| tree | 32f661f4ccd3fb36657bb9ac8104a08df9cd1d87 /pretyping/cases.ml | |
| parent | 67dc22d8389234d0c9b329944ff579e7056b7250 (diff) | |
Pretyping API using EConstr.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1a181202c..92bd1e389 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -301,7 +301,7 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = EConstr.of_constr (e_new_evar env evdref ~src:(hole_source n) (EConstr.Unsafe.to_constr ty')) in + let e = EConstr.of_constr (e_new_evar env evdref ~src:(hole_source n) ty') in (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in @@ -1665,6 +1665,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in + let ty = EConstr.of_constr ty in let ev' = e_new_evar env evdref ~src ty in let ev' = EConstr.of_constr ev' in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with @@ -1700,7 +1701,6 @@ let abstract_tycon loc env evdref subst tycon extenv t = let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in let candidates = List.map EConstr.Unsafe.to_constr candidates in - let ty = EConstr.Unsafe.to_constr ty in let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in let ev = EConstr.of_constr ev in lift k ev @@ -2469,7 +2469,6 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in let tycon = valcon_of_tycon tycon in - let tycon = Option.map EConstr.of_constr tycon in let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in let env = push_rel_context tomatchs_lets env in let len = List.length eqns in @@ -2583,7 +2582,6 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e with the type of arguments to match; if none is provided, we build alternative possible predicates *) let arsign = extract_arity_signature env tomatchs tomatchl in - let tycon = Option.map EConstr.of_constr tycon in let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = |