Merge PR #10205: Make discriminate tactic compatible with HoTT

Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot

1 files changed, 27 insertions, 28 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 51eee2a053..ec0876110b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -352,35 +352,35 @@ let find_elim hdcncl lft2rgt dep cls ot =
       (is_global_exists "core.JMeq.type" hdcncl
        && jmeq_same_dom env sigma ot)) && not dep
   then
-    let c = 
+    let c =
       match EConstr.kind sigma hdcncl with 
-      | Ind (ind_sp,u) -> 
-	let pr1 = 
+      | Ind (ind_sp,u) ->
+        let pr1 =
           lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
-	in
+        in
         begin match lft2rgt, cls with
         | Some true, None
         | Some false, Some _ ->
-	  let c1 = destConstRef pr1 in 
+          let c1 = destConstRef pr1 in
           let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
-	  let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in 
+          let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in
           let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
-	  begin 
-	    try 
-	      let _ = Global.lookup_constant c1' in
-		c1'
-	    with Not_found -> 
+          begin
+            try
+              let _ = Global.lookup_constant c1' in
+                c1'
+            with Not_found ->
 	      user_err ~hdr:"Equality.find_elim"
                 (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
 	  end
-	| _ -> destConstRef pr1
+        | _ -> destConstRef pr1
         end
       | _ -> 
 	  (* cannot occur since we checked that we are in presence of 
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-        pf_constr_of_global (ConstRef c) 
+        pf_constr_of_global (ConstRef c)
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
@@ -946,12 +946,12 @@ let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I")
 let rec build_discriminator env sigma true_0 false_0 dirn c = function
   | [] ->
       let ind = get_type_of env sigma c in
-      build_selector env sigma dirn c ind true_0 false_0
+      build_selector env sigma dirn c ind true_0 (fst false_0)
   | ((sp,cnum),argnum)::l ->
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
       let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in
-      kont sigma subval (false_0,mkProp)
+      kont sigma subval false_0
 
 (* Note: discrimination could be more clever: if some elimination is
    not allowed because of a large impredicative constructor in the
@@ -983,25 +983,22 @@ let gen_absurdity id =
           absurd_term=False
 *)
 
-let ind_scheme_of_eq lbeq =
+let ind_scheme_of_eq lbeq to_kind =
   let (mib,mip) = Global.lookup_inductive (destIndRef lbeq.eq) in
-  let kind = inductive_sort_family mip in
+  let from_kind = inductive_sort_family mip in
   (* use ind rather than case by compatibility *)
-  let kind =
-    if kind == InProp then Elimschemes.ind_scheme_kind_from_prop
-    else Elimschemes.ind_scheme_kind_from_type in
+  let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
   let c, eff = find_scheme kind (destIndRef lbeq.eq) in
     ConstRef c, eff
 
 
-let discrimination_pf e (t,t1,t2) discriminator lbeq =
+let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
   build_coq_I () >>= fun i ->
-  build_coq_False () >>= fun absurd_term ->
-  let eq_elim, eff       = ind_scheme_of_eq lbeq in
+  let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in
   Proofview.tclEFFECTS eff <*>
     pf_constr_of_global eq_elim >>= fun eq_elim ->
     Proofview.tclUNIT
-       (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term)
+       (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
 
 
 let eq_baseid = Id.of_string "e"
@@ -1018,21 +1015,23 @@ let apply_on_clause (f,t) clause =
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   build_coq_True () >>= fun true_0 ->
   build_coq_False () >>= fun false_0 ->
+  let false_ty = Retyping.get_type_of env sigma false_0 in
+  let false_kind = Retyping.get_sort_family_of env sigma false_0 in
   let e = next_ident_away eq_baseid (vars_of_env env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in
   let discriminator =
     try
       Proofview.tclUNIT
-        (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath)
+        (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath)
     with
       UserError _ as ex -> Proofview.tclZERO ex
   in
     discriminator >>= fun discriminator ->
-    discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) ->
-    let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in
+    discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
+    let pf_ty = mkArrow eqn Sorts.Relevant false_0 in
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
     let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
-    tclTHENS (assert_after Anonymous absurd_term)
+    tclTHENS (assert_after Anonymous false_0)
       [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =