1 files changed, 44 insertions, 43 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 434fb14a6e..ef894b2395 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,3 +1,4 @@
+open API
 open Printer
 open CErrors
 open Util
@@ -105,7 +106,7 @@ let make_refl_eq constructor type_of_t t  =
 
 type pte_info =
     {
-      proving_tac : (Id.t list ->  Tacmach.tactic);
+      proving_tac : (Id.t list -> Proof_type.tactic);
       is_valid : constr -> bool
     }
 
@@ -397,7 +398,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
     then tclIDTAC g
     else
       match eq_ids with
-	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
+	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.");
 	| eq_id::eq_ids ->
 	    tclTHEN
 	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
@@ -605,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
 			      pr_leconstr_env (pf_env g') (project g') new_term_value_eq
 			   );
-		   anomaly (Pp.str "cannot compute new term value")
+		   anomaly (Pp.str "cannot compute new term value.")
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
@@ -687,7 +688,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 
 let build_proof
     (interactive_proof:bool)
-    (fnames:constant list)
+    (fnames:Constant.t list)
     ptes_infos
     dyn_infos
     : tactic =
@@ -707,13 +708,13 @@ let build_proof
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
-		  tclTHENSEQ
+		  tclTHENLIST
 		    [
 		      Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
 		      thin dyn_infos.rec_hyps;
 		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
+			 tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (project g') (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -838,7 +839,7 @@ let build_proof
 		 h_reduce_with_zeta Locusops.onConcl;
 		 build_proof do_finalize new_infos
 		] g
-	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
     observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
@@ -944,7 +945,7 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
 let var_of_decl = id_of_decl %> mkVar
 let revert idl =
   tclTHEN
@@ -981,14 +982,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
   (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
-  let f_id = Label.to_id (con_label (fst (destConst evd f))) in
+  let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in
   let prove_replacement =
-    tclTHENSEQ
+    tclTHENLIST
       [
 	tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
 	observe_tac "" (fun g ->
 	   let rec_id = pf_nth_hyp_id g 1 in
-	   tclTHENSEQ
+	   tclTHENLIST
 	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
 	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
@@ -1018,7 +1019,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
-      let f_id = Label.to_id (con_label (fst (destConst !evd f))) in
+      let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
 	i*)
@@ -1032,7 +1033,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> CErrors.anomaly (Pp.str "Not a constant")
+					    | _ -> CErrors.anomaly (Pp.str "Not a constant.")
 					 )
 		}
 	  | _ -> ()
@@ -1127,11 +1128,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1158,7 +1159,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		(fun i types ->
 		   let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
-		     name = Nameops.out_name (fresh_id names.(i));
+		     name = Nameops.Name.get_id (fresh_id names.(i));
 		     types = types;
 		     offset = fix_offset;
 		     nb_realargs =
@@ -1181,7 +1182,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
 		   let app_f = mkApp(f,first_args) in
 		   let pte_args = (Array.to_list first_args)@[app_f] in
-		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
+		   let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
@@ -1208,9 +1209,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 			 num_in_block = num
 		     }
 		   in
-(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
+(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++  *)
 (* 			      str " to " ++ Ppconstr.pr_id info.name); *)
-		   (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info)
 		   )
 		0
 		(Id.Map.empty,[])
@@ -1241,7 +1242,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		other_fix_infos 0)
     in
     let first_tac : tactic = (* every operations until fix creations *)
-      tclTHENSEQ
+      tclTHENLIST
 	[ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)));
 	  observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)));
 	  observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)));
@@ -1255,11 +1256,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	try
 	  let pte =
             try destVar (project gl) pte
-            with DestKO -> anomaly (Pp.str "Property is not a variable")
+            with DestKO -> anomaly (Pp.str "Property is not a variable.")
           in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
-	  tclTHENSEQ
+	  tclTHENLIST
 	    [
 	      (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro));
 	      (fun g -> (* replacement of the function by its body *)
@@ -1278,13 +1279,13 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     eq_hyps = []
 		   }
 		 in
-		 tclTHENSEQ
+		 tclTHENLIST
 		   [
 		     observe_tac "do_replace"
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
+			  (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1321,7 +1322,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    ] gl
 	with Not_found ->
 	  let nb_args = min (princ_info.nargs) (List.length ctxt) in
-	  tclTHENSEQ
+	  tclTHENLIST
 	    [
 	      tclDO nb_args (Proofview.V82.of_tactic intro);
 	      (fun g -> (* replacement of the function by its body *)
@@ -1342,7 +1343,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   }
 		 in
 		 let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in
-		 tclTHENSEQ
+		 tclTHENLIST
 		   [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
 		    let do_prove =
 		      build_proof
@@ -1401,7 +1402,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 	fun gls ->
 (* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
 (* 	  let ids = hid::pf_ids_of_hyps gls in  *)
-	  tclTHENSEQ
+	  tclTHENLIST
 	    [
 (* 	      generalize [lemma]; *)
 (* 	      h_intro hid; *)
@@ -1456,13 +1457,13 @@ let rec rewrite_eqs_in_eqs eqs =
 
 let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
   fun gls ->
-    (tclTHENSEQ
+    (tclTHENLIST
        [
 	 backtrack_eqs_until_hrec hrec eqs;
 	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
 	    (Proofview.V82.of_tactic (apply (mkVar hrec)))
-	    [ tclTHENSEQ
+	    [ tclTHENLIST
 		[
 		  (Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
 		  (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
@@ -1481,7 +1482,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
 				      (true,5)
-				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+				      [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
 				      [Hints.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
@@ -1563,17 +1564,17 @@ let prove_principle_for_gen
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
-  let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
+  let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
   let acc_rec_arg_id =
-    Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
+    Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
     tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
-  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+  let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
@@ -1591,7 +1592,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
+  let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
@@ -1616,7 +1617,7 @@ let prove_principle_for_gen
 	  (Id.of_string "prov")
 	  hyps
       in
-      tclTHENSEQ
+      tclTHENLIST
 	[
 	  Proofview.V82.of_tactic (generalize [lemma]);
 	  Proofview.V82.of_tactic (Simple.intro hid);
@@ -1635,11 +1636,11 @@ let prove_principle_for_gen
 	  ]
 	  gls
   in
-  tclTHENSEQ
+  tclTHENLIST
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (get_name %> Nameops.out_name)
+	(List.rev_map (get_name %> Nameops.Name.get_id)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1677,14 +1678,14 @@ let prove_principle_for_gen
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
 	 let predicates_names =
-	   List.map (get_name %> Nameops.out_name) princ_info.predicates
+	   List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
 	       (fun eqs ->
 (* 		  msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id  !tcc_list); *)
-(* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
-(* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
+(* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+(* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
 (* 		  msgnl (str "acc_rec_arg_id := "++  Ppconstr.pr_id acc_rec_arg_id); *)
 (* 		  msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id  eqs); *)
 
@@ -1693,7 +1694,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (get_name %> Nameops.out_name)
+			   (get_name %> Nameops.Name.get_id)
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1722,7 +1723,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (get_name %> Nameops.out_name) princ_info.branches)
+	      (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'