Merge branch 'v8.5' into v8.6

1 files changed, 57 insertions, 54 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index aff60eaa4..fd46d8069 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -82,8 +82,10 @@ let rec decompose_term env sigma t=
     | Proj (p, c) -> 
 	let canon_const kn = constant_of_kn (canonical_con kn) in 
 	let p' = Projection.map canon_const p in
-	  (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
-    | _ ->if closed0 t then (Symb t) else raise Not_found
+	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
+    | _ ->
+       let t = strip_outer_cast t in
+       if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
 open Globnames
@@ -233,10 +235,10 @@ let build_projection intype (cstr:pconstructor) special default gls=
 
 let _M =mkMeta
 
-let app_global f args k = 
+let app_global f args k =
   Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_app_global f args k = 
+let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
@@ -246,7 +248,19 @@ let assert_before n c =
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end }
-    
+
+let refresh_type env evm ty =
+  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
+			      (Some false) env evm ty
+
+let refresh_universes ty k =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let evm = Tacmach.New.project gl in
+    let evm, ty = refresh_type env evm ty in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
+  end }
+
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
@@ -256,35 +270,31 @@ let rec proof_tac p : unit Proofview.tactic =
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
-        let typ = (* Termops.refresh_universes *) type_of l in
-        new_app_global _sym_eq [|typ;r;l;c|] exact_check
+	refresh_universes (type_of l) (fun typ ->
+        new_app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
 	let lr = constr_of_term t in
-	let typ = (* Termops.refresh_universes *) type_of lr in
-        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check
+	refresh_universes (type_of lr) (fun typ ->
+        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = (* Termops.refresh_universes *) (type_of t2) in
+	refresh_universes (type_of t2) (fun typ ->
 	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
-          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]
+          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = (* Termops.refresh_universes  *)(type_of tf1) in
-	let typx = (* Termops.refresh_universes *) (type_of tx1) in
-	let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in
+	refresh_universes (type_of tf1) (fun typf ->
+	refresh_universes (type_of tx1) (fun typx ->
+	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 =
-	  app_global _f_equal
-		[|typf;typfx;appx1;tf1;tf2;_M 1|] in
-	let lemma2=
-	  app_global _f_equal
-		[|typx;typfx;tf2;tx1;tx2;_M 1|] in
+	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
+	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
 	let prf =
 	  app_global _trans_eq
 		[|typfx;
@@ -298,34 +308,33 @@ let rec proof_tac p : unit Proofview.tactic =
 		reflexivity;
                 Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")]]
+		       "I don't know how to handle dependent equality")]])))
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype = (* Termops.refresh_universes *) (type_of ti) in
-	 let outtype = (* Termops.refresh_universes *) (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
+	 refresh_universes (type_of ti) (fun intype ->
+         refresh_universes (type_of default) (fun outtype ->
          let proj =
            Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
 	 let injt=
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
 let refute_tac c t1 t2 p =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
-  in
-  let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
+  let k intype =
+    let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
 let refine_exact_check c gl =
@@ -335,16 +344,15 @@ let refine_exact_check c gl =
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
-  in
-  let neweq= new_app_global _eq [|sort;tt1;tt2|] in
-  let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
-  let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-  let identity=mkLambda (Name x,sort,mkRel 1) in
-  let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+  let k sort =
+    let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+    let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+    let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let identity=mkLambda (Name x,sort,mkRel 1) in
+    let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -360,33 +368,28 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
 let discriminate_tac (cstr,u as cstru) p =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-    let intype =
-      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
-    in
+    let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
-    (* let outsort = mkSort outsort in *)
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-    (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
-    (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
     let identity = Universes.constr_of_global (Lazy.force _I) in
-    (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in 
+    let evm = Tacmach.New.project gl in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
-    let pred=mkLambda(Name xid,outtype,mkRel 1) in
+    let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
     let injt=app_global _f_equal
-                    [|intype;outtype;proj;t1;t2;mkVar hid|] in
+			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
-        app_global _eq_rect
-          [|outtype;trivial;pred;identity;concl;injt|] k) in
+            app_global _eq_rect
+		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
-      (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-        [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
   end }
 
 (* wrap everything *)
@@ -470,7 +473,7 @@ let congruence_tac depth l =
    This isn't particularly related with congruence, apart from
    the fact that congruence is called internally.
 *)
-    
+
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -482,7 +485,7 @@ let mk_eq f c1 c2 k =
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
     end })
-    
+
 let f_equal =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in