Merge tag 'upstream/8.6'

Upstream version 8.6

12 files changed, 81 insertions, 59 deletions

diff --git a/AAC.v b/AAC.v
index f6f382f..5feb0b6 100644
--- a/AAC.v
+++ b/AAC.v
@@ -1115,6 +1115,11 @@ Section s.
 End s.
 End Internal.
 
+Local Ltac internal_normalize :=
+  let x := fresh in let y := fresh in
+  intro x; intro y; vm_compute in x; vm_compute in y; unfold x; unfold y;
+  compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl.
+
 
 (** * Lemmas for performing transitivity steps
    given an instance of AAC_lift *)
diff --git a/Make b/Make
index 8caf805..ec45b23 100644
--- a/Make
+++ b/Make
@@ -1,5 +1,6 @@
 -I .
 -R . AAC_tactics
+
 coq.mli
 helper.mli
 search_monad.mli
@@ -15,6 +16,7 @@ theory.ml
 print.ml
 rewrite.ml4
 aac.mlpack
+
 AAC.v
 Instances.v
 Tutorial.v
diff --git a/Makefile b/Makefile
index a9d5466..abf2ec6 100644
--- a/Makefile
+++ b/Makefile
@@ -8,6 +8,8 @@ clean: Makefile.coq
 Makefile.coq: Make
 	$(COQBIN)coq_makefile -f Make -o Makefile.coq
 
+Make: ;
+
 %: Makefile.coq
 	+make -f Makefile.coq $@
 
diff --git a/coq.ml b/coq.ml
index 97154e2..eb4b5f1 100755
--- a/coq.ml
+++ b/coq.ml
@@ -12,6 +12,8 @@ type constr = Term.constr
 open Term
 open Names
 open Coqlib
+open Sigma.Notations
+open Context.Rel.Declaration
 
 (* The contrib name is used to locate errors when loading constrs *)
 let contrib_name = "aac_tactics"
@@ -55,7 +57,9 @@ let goal_update (goal : goal_sigma) evar_map : goal_sigma=
 let fresh_evar goal ty : constr * goal_sigma =
   let env = Tacmach.pf_env goal in
   let evar_map = Tacmach.project goal in
-  let (em,x) = Evarutil.new_evar env evar_map ty in
+  let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+  let Sigma (x,em,_) = Evarutil.new_evar env evar_map ty in
+  let em = Sigma.to_evar_map em in
     x,( goal_update goal em)
      
 let resolve_one_typeclass goal ty : constr*goal_sigma=
@@ -73,8 +77,8 @@ let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr  -> Proof_type
 		  try Typeclasses.resolve_one_typeclass env em t
 		  with Not_found ->
 		    begin match error with
-		      | None -> Errors.anomaly (Pp.str "Cannot resolve a typeclass : please report")
-		      | Some x -> Errors.error x
+		      | None -> CErrors.anomaly (Pp.str "Cannot resolve a typeclass : please report")
+		      | Some x -> CErrors.error x
 		    end
 		in
 		Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal
@@ -88,28 +92,36 @@ let nf_evar goal c : Term.constr=
 let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma =
   let env = Tacmach.pf_env gl in
   let evar_map = Tacmach.project gl in
-  let (em,x) = Evarutil.new_evar env evar_map x in
+  let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+  let Sigma (x,em,_) = Evarutil.new_evar env evar_map x in
+  let em = Sigma.to_evar_map em in
     x,(goal_update gl em)
      
 let evar_binary (gl: goal_sigma) (x : constr) =
   let env = Tacmach.pf_env gl in
   let evar_map = Tacmach.project gl in
   let ty = mkArrow x (mkArrow x x) in
-  let (em,x) = Evarutil.new_evar env evar_map ty in
+  let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+  let Sigma (x,em,_) = Evarutil.new_evar env evar_map ty in
+  let em = Sigma.to_evar_map em in
     x,( goal_update gl em)
 
 let evar_relation (gl: goal_sigma) (x: constr) =
   let env = Tacmach.pf_env gl in
   let evar_map = Tacmach.project gl in
   let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
-  let (em,r) = Evarutil.new_evar env evar_map ty in
+  let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+  let Sigma (r, em, _) = Evarutil.new_evar env evar_map ty in
+  let em = Sigma.to_evar_map em in
     r,( goal_update gl em)
 
 let cps_evar_relation (x: constr) k = fun goal -> 
   Tacmach.pf_apply
     (fun env em ->
       let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
-      let (em,r) = Evarutil.new_evar env em ty in
+      let em = Sigma.Unsafe.of_evar_map em in
+      let Sigma (r, em, _) = Evarutil.new_evar env em ty in
+      let em = Sigma.to_evar_map em in
       Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal
     )	goal
 
@@ -319,9 +331,9 @@ module Equivalence = struct
 end
 end
 (**[ match_as_equation goal eqt] see [eqt] as an equation. An
-   optionnal rel_context can be provided to ensure taht the term
+   optionnal rel-context can be provided to ensure that the term
    remains typable*)
-let match_as_equation ?(context = Context.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option  =
+let match_as_equation ?(context = Context.Rel.empty) goal equation : (constr*constr* Std.Relation.t) option  =
   let env = Tacmach.pf_env goal in
   let env =  Environ.push_rel_context context env in
   let evar_map = Tacmach.project goal in
@@ -345,15 +357,15 @@ let match_as_equation ?(context = Context.empty_rel_context) goal equation : (co
 let tclTIME msg tac = fun gl ->
   let u = Sys.time () in
   let r = tac gl in
-  let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-.  u))) in
+  let _ = Feedback.msg_notice (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-.  u))) in
     r
 
 let tclDEBUG msg tac = fun gl ->
-  let _ = Pp.msgnl (Pp.str msg) in
+  let _ = Feedback.msg_debug (Pp.str msg) in
     tac gl
 
 let tclPRINT  tac = fun gl ->
-  let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in
+  let _ = Feedback.msg_notice (Printer.pr_constr (Tacmach.pf_concl gl)) in
     tac gl
 
 
@@ -361,13 +373,13 @@ let tclPRINT  tac = fun gl ->
 (* functions to handle the failures of our tactic. Some should be
    reported [anomaly], some are on behalf of the user [user_error]*)
 let anomaly msg =
-  Errors.anomaly ~label:"[aac_tactics]" (Pp.str msg)
+  CErrors.anomaly ~label:"[aac_tactics]" (Pp.str msg)
 
 let user_error msg =
-  Errors.error ("[aac_tactics] " ^ msg)
+  CErrors.error ("[aac_tactics] " ^ msg)
 
 let warning msg =
-  Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg))
+  Feedback.msg_warning (Pp.str ("[aac_tactics]" ^ msg))
 
      
 (** {1 Rewriting tactics used in aac_rewrite}  *)
@@ -384,7 +396,7 @@ type hypinfo =
     {
       hyp : Term.constr;		  (** the actual constr corresponding to the hypothese  *)
       hyptype : Term.constr; 		(** the type of the hypothesis *)
-      context : Context.rel_context; 	(** the quantifications of the hypothese *)
+      context : Context.Rel.t;       	(** the quantifications of the hypothese *)
       body : Term.constr; 		(** the body of the type of the hypothesis*)
       rel : Std.Relation.t; 		(** the relation  *)
       left : Term.constr;		(** left hand side *)
@@ -397,16 +409,14 @@ let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proo
   let (rel_context, body_type) = Term.decompose_prod_assum ctype in 
   let rec check f e =
     match decomp_term e with
-      | Term.Rel i ->
-	    let name, constr_option, types = Context.lookup_rel i rel_context
-	    in f types
+      | Term.Rel i -> f (get_type (Context.Rel.lookup i rel_context))
       | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e
   in
   begin match check_type with
     | None -> ()
     | Some f ->
-      if not (check f body_type)
-      then user_error "Unable to deal with higher-order or heterogeneous patterns";
+	if not (check f body_type)
+	then user_error "Unable to deal with higher-order or heterogeneous patterns";
   end;
   begin
     match match_as_equation ~context:rel_context  goal body_type with
@@ -443,7 +453,7 @@ let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proo
 (* Fresh evars for everyone (should be the good way to do this
    recompose in Coq v8.4) *)
 let recompose_prod 
-    (context : Context.rel_context)
+    (context : Context.Rel.t)
     (subst : (int * Term.constr) list)
     env
     em
@@ -457,14 +467,17 @@ let recompose_prod
     match context with
       | [] ->
 	env, em, acc
-      | ((name,c,ty) as t)::q ->
+      | t::q ->
 	let env, em, acc = aux q acc em (n+1) in
 	if n >= min_n
 	then
 	  let em,x =
 	    try em, List.assoc n subst
 	    with | Not_found ->
-	      Evarutil.new_evar env em (Vars.substl acc ty)
+              let em = Sigma.Unsafe.of_evar_map em in
+	      let Sigma (r, em, _) = Evarutil.new_evar env em (Vars.substl acc (get_type t)) in
+              let em = Sigma.to_evar_map em in
+              (em, r)
 	  in
 	  (Environ.push_rel t env), em,x::acc
 	else
@@ -477,7 +490,7 @@ let recompose_prod
    application to handle non-instanciated variables. *)
    
 let recompose_prod'
-    (context : Context.rel_context)
+    (context : Context.Rel.t)
     (subst : (int *Term.constr) list)
     c
     =
@@ -487,7 +500,7 @@ let recompose_prod'
       | [] -> []
       | t::q -> pop t :: (popn pop (n-1) q)
   in
-  let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in
+  let pop_rel_decl = map_type Termops.pop in
   let rec aux sign n next app ctxt =
     match sign with
       | [] -> List.rev app, List.rev ctxt
diff --git a/coq.mli b/coq.mli
index 1004d2c..4d46c7d 100644
--- a/coq.mli
+++ b/coq.mli
@@ -147,9 +147,9 @@ module Equivalence : sig
 end
 
 (** [match_as_equation ?context goal c] try to decompose c as a
-    relation applied to two terms. An optionnal rel_context can be
+    relation applied to two terms. An optionnal rel-context can be
     provided to ensure that the term remains typable *)
-val match_as_equation  : ?context:Context.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option
+val match_as_equation  : ?context:Context.Rel.t -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option
 
 (** {2 Some tacticials}  *)
 
@@ -190,7 +190,7 @@ type hypinfo =
     {
       hyp : Term.constr;		  (** the actual constr corresponding to the hypothese  *)
       hyptype : Term.constr; 		(** the type of the hypothesis *)
-      context : Context.rel_context; 	(** the quantifications of the hypothese *)
+      context : Context.Rel.t;		(** the quantifications of the hypothese *)
       body : Term.constr; 		(** the body of the hypothese*)
       rel : Relation.t; 		(** the relation  *)
       left : Term.constr;		(** left hand side *)
diff --git a/helper.ml b/helper.ml
index 637def1..636b17f 100644
--- a/helper.ml
+++ b/helper.ml
@@ -29,8 +29,8 @@ module Debug (X : CONTROL) = struct
 
   let pr_constr msg constr =
     if printing then
-      (  Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg));
-	 Pp.msgnl (Printer.pr_constr constr);
+      (  Feedback.msg_notice (Pp.str (Printf.sprintf "=====%s====" msg));
+	 Feedback.msg_notice (Printer.pr_constr constr);
       )
 
 
diff --git a/matcher.ml b/matcher.ml
index 2fd0517..1dcb1d2 100644
--- a/matcher.ml
+++ b/matcher.ml
@@ -455,7 +455,7 @@ end
        | Dot (s,l,r) -> Dot (s, aux l, aux r)
        | Var i -> 
 	   begin match find t i  with
-	     | None -> Errors.error "aac_tactics: instantiate failure"
+	     | None -> CErrors.error "aac_tactics: instantiate failure"
 	     | Some x -> t_of_term  x
 	   end
      in aux x
@@ -1092,7 +1092,7 @@ let unit_warning p ~nullif ~unitif =
   if not (Search.is_empty unitif)
   then
     begin
-      Pp.msg_warning
+      Feedback.msg_warning
 	(Pp.str
 	   "[aac_tactics] This pattern can be instanciated to match units, some solutions can be missing");
     end
diff --git a/print.ml b/print.ml
index 0305158..427b6dc 100644
--- a/print.ml
+++ b/print.ml
@@ -10,6 +10,8 @@
    solution *)
 open Pp
 open Matcher
+open Context.Rel.Declaration
+
 type named_env = (Names.name * Terms.t) list
  
 
@@ -65,14 +67,14 @@ let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.
 rename the variables, and rebuilds raw Coq terms (for the context, and
 the terms in the environment). In order to do so, it requires the
 information gathered by the {!Theory.Trans} module.*)
-let print rlt ir m (context : Context.rel_context) goal =
+let print rlt ir m (context : Context.Rel.t) goal =
   if Search_monad.count m = 0
   then
     (
       Tacticals.tclFAIL 0  (Pp.str "No subterm modulo AC")  goal
     )
   else
-    let _ = Pp.msgnl (Pp.str "All solutions:") in
+    let _ = Feedback.msg_notice (Pp.str "All solutions:") in
     let m = Search_monad.(>>) m
       (fun (i,t,envm) ->
 	let envm = Search_monad.(>>) envm ( fun env ->
@@ -80,8 +82,7 @@ let print rlt ir m (context : Context.rel_context) goal =
 	  let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in
 	  let l =
 	    List.map (fun (v,t) ->
-	      let (name,body,types) = Context.lookup_rel  v context in
-	      (name,t)
+	      get_name (Context.Rel.lookup v context), t
 	    ) l
 	  in
 	  Search_monad.return l
@@ -91,7 +92,7 @@ let print rlt ir m (context : Context.rel_context) goal =
       )
     in
     let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x -  y) m in
-    let _ = Pp.msgnl
+    let _ = Feedback.msg_notice
       (pp_all
 	 (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t ir rlt  context  t) ) m
       )
diff --git a/print.mli b/print.mli
index 7fab3be..bbb9b20 100644
--- a/print.mli
+++ b/print.mli
@@ -10,7 +10,7 @@
     tactic. *)
 
 
-(** The main printing function. {!print} uses the [Term.rel_context]
+(** The main printing function. {!print} uses the rel-context
     to rename the variables, and rebuilds raw Coq terms (for the given
     context, and the terms in the environment). In order to do so, it
     requires the information gathered by the {!Theory.Trans} module.*)
@@ -18,6 +18,6 @@ val print :
   Coq.Relation.t ->
   Theory.Trans.ir ->
   (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
-  Context.rel_context  ->
+  Context.Rel.t  ->
   Proof_type.tactic
 
diff --git a/rewrite.ml4 b/rewrite.ml4
index b3e52e0..1f57c0b 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -8,6 +8,11 @@
 
 (** aac_rewrite -- rewriting modulo  *)
 
+open Pcoq.Prim
+open Pcoq.Constr
+open Stdarg
+open Constrarg
+
 DECLARE PLUGIN "aac"
 
 module Control =   struct
@@ -33,7 +38,7 @@ let retype = Coq.retype
 (* helper to be used with the previous function: raise a new anomaly
    except if a another one was previously raised *)
 let push_anomaly msg = function
-  | e when Errors.is_anomaly e -> raise e
+  | e when CErrors.is_anomaly e -> raise e
   | _ -> Coq.anomaly msg
 
 module M = Matcher
@@ -190,7 +195,7 @@ let by_aac_reflexivity zero
 	 [ retype decision_thm; retype convert_to;
 	   convert ;
 	   tac_or_exn apply_tac Coq.user_error "unification failure";
-	   tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure";
+	   tac_or_exn (time_tac "vm_norm" (Proofview.V82.of_tactic (Tactics.normalise_in_concl))) Coq.anomaly "vm_compute failure";
 	   Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity)
 	     (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
 	 ])
@@ -253,25 +258,19 @@ let aac_conclude
     | Not_found -> Coq.user_error "No lifting from the goal's relation to an equivalence"
 
 open Libnames
+open Tacexpr
 open Tacinterp
 
 let aac_normalise = fun goal ->
   let ids = Tacmach.pf_ids_of_hyps goal in
+  let loc = Loc.ghost in
+  let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in
+  let norm_tac = KerName.make2 mp (Label.make "internal_normalize") in
+  let norm_tac = Misctypes.ArgArg (loc, norm_tac) in
   Tacticals.tclTHENLIST
     [
       aac_conclude by_aac_normalise;
-      Proofview.V82.of_tactic begin
-      Tacinterp.interp (
-      	<:tactic<
-	  intro x;
-	  intro y;
-	  vm_compute in x;
-	  vm_compute in y;
-	  unfold x;
-	  unfold y;
-      	  compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl
-      	>>
-      )end;
+      Proofview.V82.of_tactic (Tacinterp.eval_tactic (TacArg (loc, TacCall (loc, norm_tac, []))));
       Proofview.V82.of_tactic (Tactics.keep ids)
     ] goal
 
diff --git a/theory.ml b/theory.ml
index a5229fa..20cb299 100644
--- a/theory.ml
+++ b/theory.ml
@@ -289,10 +289,10 @@ module Unit = struct
 end
 
 let anomaly msg =
-  Errors.anomaly ~label:"aac_tactics" (Pp.str msg)
+  CErrors.anomaly ~label:"aac_tactics" (Pp.str msg)
 
 let user_error msg =
-  Errors.error ("aac_tactics: " ^ msg)
+  CErrors.error ("aac_tactics: " ^ msg)
 
 module Trans = struct
  
@@ -877,11 +877,11 @@ module Trans = struct
       t , get ( )
 
   (** [raw_constr_of_t] rebuilds a term in the raw representation *)
-  let raw_constr_of_t ir rlt (context:rel_context) t =
+  let raw_constr_of_t ir rlt (context:Context.Rel.t) t =
       (** cap rebuilds the products in front of the constr *)
     let rec cap c = function [] -> c
       | t::q -> 
-	  let i = Context.lookup_rel t context in
+	  let i = Context.Rel.lookup t context in
 	  cap (mkProd_or_LetIn i c) q
     in
     let t,indices = raw_constr_of_t_debruijn ir t in
diff --git a/theory.mli b/theory.mli
index 1dae57b..fe79a11 100644
--- a/theory.mli
+++ b/theory.mli
@@ -160,7 +160,7 @@ module Trans :  sig
       reconstruct the named products on top of it. In particular, this
       allow us to print the context put around the left (or right)
       hand side of a pattern. *)
-  val raw_constr_of_t : ir ->  Coq.Relation.t -> (Context.rel_context)  ->Matcher.Terms.t -> Term.constr
+  val raw_constr_of_t : ir ->  Coq.Relation.t -> (Context.Rel.t)  ->Matcher.Terms.t -> Term.constr
 
   (** {2 Building reified terms} *)