aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/subtac/subtac_cases.ml76
-rw-r--r--plugins/subtac/subtac_coercion.ml1
2 files changed, 38 insertions, 39 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 00ed62ac8..26507a1ca 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1828,24 +1828,6 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
* A type constraint but no annotation case: it is assumed non dependent.
*)
-
-let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
- (* We extract the signature of the arity *)
- let arsign = extract_arity_signature env tomatchs sign in
- let env = List.fold_right push_rels arsign env in
- let allnames = List.rev (List.map (List.map pi1) arsign) in
- match rtntyp with
- | Some rtntyp ->
- let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
- let predccl = (j_nf_isevar !isevars predcclj).uj_val in
- Some (build_initial_predicate true allnames predccl)
- | None ->
- match valcon_of_tycon tycon with
- | Some ty ->
- let names,pred =
- oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty
- in Some (build_initial_predicate true names pred)
- | None -> None
let lift_ctx n ctx =
let ctx', _ =
@@ -2025,6 +2007,25 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
ignore(Typing.sort_of env' evm pred); pred
with _ -> lift nar c
+
+let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
+ (* We extract the signature of the arity *)
+ let arsign = extract_arity_signature env tomatchs sign in
+ let newenv = List.fold_right push_rels arsign env in
+ let allnames = List.rev (List.map (List.map pi1) arsign) in
+ match rtntyp with
+ | Some rtntyp ->
+ let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
+ let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ Some (build_initial_predicate true allnames predccl)
+ | None ->
+ match valcon_of_tycon tycon with
+ | Some ty ->
+ let pred =
+ prepare_predicate_from_arsign_tycon loc env !isevars tomatchs arsign ty
+ in Some (build_initial_predicate true allnames pred)
+ | None -> None
+
let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
let typing_fun tycon env = typing_fun tycon env isevars in
@@ -2103,26 +2104,25 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
(* with the type of arguments to match *)
let tmsign = List.map snd tomatchl in
let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
-
- (* We push the initial terms to match and push their alias to rhs' envs *)
- (* names of aliases will be recovered from patterns (hence Anonymous here) *)
- let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-
- let pb =
- { env = env;
- isevars = isevars;
- pred = pred;
- tomatch = initial_pushed;
- history = start_history (List.length initial_pushed);
- mat = matx;
- caseloc = loc;
- casestyle= style;
- typing_function = typing_fun } in
-
- let j = compile pb in
- (* We check for unused patterns *)
- List.iter (check_unused_pattern env) matx;
- inh_conv_coerce_to_tycon loc env isevars j tycon
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ casestyle= style;
+ typing_function = typing_fun } in
+
+ let j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ inh_conv_coerce_to_tycon loc env isevars j tycon
+
end
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 54114b0b0..ce7b5431b 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -454,7 +454,6 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
- let evd = nf_evar_defs evd in
match n with
None ->
let (evd', val') =