Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

9 files changed, 44 insertions, 36 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 3c4cacbc54..9d78a51ef6 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -99,4 +99,4 @@ type proof_instr =
     (Term.constr statement,
      Term.constr,
      proof_pattern,
-     Tacexpr.glob_tactic_expr) gen_proof_instr
+     Genarg.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 1c56586cea..34307a358f 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -96,7 +96,7 @@ let rec add_vars_of_simple_pattern globs = function
       add_vars_of_simple_pattern globs p
   | CPatCstr (_,_,pl1,pl2) ->
     List.fold_left add_vars_of_simple_pattern
-      (List.fold_left add_vars_of_simple_pattern globs pl1) pl2
+      (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2
   | CPatNotation(_,_,(pl,pll),pl') ->
       List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll))
   | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
@@ -384,7 +384,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 
 let interp_cut interp_it env sigma cut=
   let nenv,nstat = interp_it env sigma cut.cut_stat in
-    {cut with
+    { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
        cut_stat=nstat;
        cut_by=interp_justification_items nenv sigma cut.cut_by}
 
@@ -403,7 +403,7 @@ let interp_suffices_clause env sigma (hyps,cot)=
     match hyp with
 	(Hprop st | Hvar st) ->
 	  match st.st_label with
-	      Name id -> Environ.push_named (id,None,st.st_it) env0
+	      Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0
 	    | _ -> env in
   let nenv = List.fold_right push_one locvars env in
     nenv,res
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
index b3d6f82bd9..4303ecdb42 100644
--- a/plugins/decl_mode/decl_interp.mli
+++ b/plugins/decl_mode/decl_interp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 774c20c9ae..f9399d6824 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -116,7 +116,7 @@ let get_top_stack pts =
 let get_stack pts = Proof.get_at_focus proof_focus pts
 
 let get_last env = match Environ.named_context env with
-  | (id,_,_)::_ -> id
+  | decl :: _ -> Context.Named.Declaration.get_id decl
   | [] -> error "no previous statement to use"
 
 
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index fd7e15c150..dfeee833cb 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 714cd86341..090b293f5c 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,6 +29,8 @@ open Termops
 open Namegen
 open Goptions
 open Misctypes
+open Sigma.Notations
+open Context.Named.Declaration
 
 (* Strictness option *)
 
@@ -86,7 +88,7 @@ Please \"suppose\" something or \"end\" it now."
       | _ -> ()
 
 let mk_evd metalist gls =
-  let evd0= create_goal_evar_defs (sig_sig gls) in
+  let evd0= clear_metas (sig_sig gls) in
   let add_one (meta,typ) evd =
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
@@ -212,7 +214,7 @@ let close_previous_case pts =
     Proof.is_done pts
   then
     match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
+	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
       | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
@@ -228,7 +230,8 @@ let close_previous_case pts =
 (* automation *)
 
 let filter_hyps f gls =
-  let filter_aux (id,_,_) =
+  let filter_aux id =
+    let id = get_id id in
     if f id then
       tclIDTAC
     else
@@ -330,11 +333,12 @@ let enstack_subsubgoals env se stack gls=
 	    let rc,_ = Reduction.dest_prod env apptype in
 	    let rec meta_aux last lenv = function
 		[] -> (last,lenv,[])
-	      | (nam,_,typ)::q ->
+	      | decl::q ->
 		  let nlast=succ last in
 		  let (llast,holes,metas) =
 		    meta_aux nlast (mkMeta nlast :: lenv) q in
-		    (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
+                    let open Context.Rel.Declaration in
+		    (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in
 	    let (nlast,holes,nmetas) =
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
@@ -403,15 +407,15 @@ let concl_refiner metas body gls =
   let concl = pf_concl gls in
   let evd = sig_sig gls in
   let env = pf_env gls in
-  let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in
+  let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
   let rec aux env avoid subst = function
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
 	let _A = subst_meta subst typ in
 	let x = id_of_name_using_hdchar env _A Anonymous in
 	let _x = fresh_id avoid x gls in
-	let nenv = Environ.push_named (_x,None,_A) env in
-	let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in
+	let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
+	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
 	let nsubst = (n,mkVar _x)::subst in
 	  if List.is_empty rest then
 	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
@@ -492,7 +496,7 @@ let just_tac _then cut info gls0 =
         None ->
 	  Proofview.V82.of_tactic automation_tac gls
       | Some tac ->
-	  Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+	  Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
     justification (tclTHEN items_tac method_tac) gls0
 
 let instr_cut mkstat _thus _then cut gls0 =
@@ -542,7 +546,7 @@ let instr_rew _thus rew_side cut gls0 =
         None ->
 	  Proofview.V82.of_tactic automation_tac gls
       | Some tac ->
-	  Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+	  Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
   let just_tac gls =
     justification (tclTHEN items_tac method_tac) gls in
   let (c_id,_) = match cut.cut_stat.st_label with
@@ -605,7 +609,7 @@ let assume_tac hyps gls =
        tclTHEN
 	 (push_intro_tac
 	    (fun id ->
-	       Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+	       Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
 	 hyps tclIDTAC gls
 
 let assume_hyps_or_theses hyps gls =
@@ -615,7 +619,7 @@ let assume_hyps_or_theses hyps gls =
 	   tclTHEN
 	     (push_intro_tac
 		(fun id ->
-		   Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam)
+		   Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam)
        | Hprop {st_label=nam;st_it=Thesis (tk)} ->
 	   tclTHEN
 	     (push_intro_tac
@@ -627,7 +631,7 @@ let assume_st hyps gls =
     (fun st ->
        tclTHEN
 	 (push_intro_tac
-	    (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+	    (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
 	 hyps tclIDTAC gls
 
 let assume_st_letin hyps gls =
@@ -636,7 +640,7 @@ let assume_st_letin hyps gls =
        tclTHEN
 	 (push_intro_tac
 	    (fun id ->
-	       Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label))
+	       Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label))
 	 hyps tclIDTAC gls
 
 (* suffices *)
@@ -730,7 +734,7 @@ let rec consider_match may_intro introduced available expected gls =
 	  error "Not enough sub-hypotheses to match statements."
 	    (* should tell which ones *)
     | id::rest_ids,(Hvar st | Hprop st)::rest ->
-	tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it)))
+	tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it))))
 	  begin
 	    match st.st_label with
 		Anonymous ->
@@ -798,8 +802,8 @@ let define_tac id args body gls =
 let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
       This id ->
-	let (_,body,_) = pf_get_hyp gls id in
-	  Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls
+	let body = pf_get_hyp gls id |> get_value in
+	  Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
@@ -1305,7 +1309,11 @@ let understand_my_constr env sigma c concl =
   Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
 
 let my_refine c gls =
-  let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+  let oc = { run = begin fun sigma ->
+    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+    Sigma.Unsafe.of_pair (c, sigma)
+  end } in
   Proofview.V82.of_tactic (Tactics.New.refine oc) gls
 
 (* end focus/claim *)
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index f86bfea712..325969dadb 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index d598e7c3fa..a438ca79f4 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -87,7 +87,7 @@ let vernac_proof_instr instr =
 
 (* Only declared at raw level, because only used in vernac commands. *)
 let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
-  Genarg.make0 None "proof_instr"
+  Genarg.make0 "proof_instr"
 
 (* We create a new parser entry [proof_mode]. The Declarative proof mode
     will replace the normal parser entry for tactics with this one. *)
@@ -95,7 +95,7 @@ let proof_mode : vernac_expr Gram.entry =
   Gram.entry_create "vernac:proof_command"
 (* Auxiliary grammar entry. *)
 let proof_instr : raw_proof_instr Gram.entry =
-  Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr)
+  Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
@@ -135,7 +135,7 @@ let _ =
 				       set = begin fun () ->
 					 (* We set the command non terminal to
 					     [proof_mode] (which we just defined). *)
-					 G_vernac.set_command_entry proof_mode ;
+					 Pcoq.set_command_entry proof_mode ;
 					 (* We substitute the goal printer, by the one we built
 					     for the proof mode. *)
 					 Printer.set_printer_pr { Printer.default_printer_pr with
@@ -147,7 +147,7 @@ let _ =
 				       reset = begin fun () ->
 					 (* We restore the command non terminal to
 					      [noedit_mode]. *)
-					 G_vernac.set_command_entry G_vernac.noedit_mode ;
+					 Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
 					 (* We restore the goal printer to default *)
 					 Printer.set_printer_pr Printer.default_printer_pr
 				       end
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index b3198dbf24..4c71f04107 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)