Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

14 files changed, 106 insertions, 13 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 3f232c36..a7241399 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -55,6 +55,9 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
 
 let wit_bindings = unsafe_of_type BindingsArgType
 
+let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
+  Genarg.make0 None "hyp_location_flag"
+
 let wit_red_expr = unsafe_of_type RedExprArgType
 
 let wit_clause_dft_concl  =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 74c6bd31..fdeddd66 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -64,6 +64,8 @@ val wit_bindings :
   glob_constr_and_expr bindings,
   constr bindings Evd.sigma) genarg_type
 
+val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
+
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 58e1eb1d..f57772ec 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -977,7 +977,7 @@ let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
   | PVar id -> GVar (loc,id)
   | PEvar (evk,l) ->
-      let test id = function PVar id' -> Id.equal id id' | _ -> false in
+      let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
       let id = Evd.evar_ident evk sigma in
       GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 68f0050d..5151d2a1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1567,7 +1567,6 @@ let internalize globalenv env allow_patvar lvar c =
           let lvars = Id.Set.union lvars env.ids in
           let ist = {
             Genintern.ltacvars = lvars;
-            ltacrecvars = Id.Map.empty;
             genv = globalenv;
           } in
           let (_, glb) = Genintern.generic_intern ist gen in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 792e6f63..0d33d433 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -174,6 +174,7 @@ val interp_context_evars :
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
+val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
 val construct_reference : named_context -> Id.t -> constr
 val global_reference : Id.t -> constr
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index e722615a..02504c92 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -349,7 +349,6 @@ let build_coq_inversion_eq_true_data () =
 
 (* The False proposition *)
 let coq_False  = lazy_init_constant ["Logic"] "False"
-let coq_proof_admitted = lazy_init_constant ["Logic"] "proof_admitted"
 
 (* The True proposition and its unique proof *)
 let coq_True   = lazy_init_constant ["Logic"] "True"
@@ -371,7 +370,6 @@ let build_coq_True ()  = Lazy.force coq_True
 let build_coq_I ()     = Lazy.force coq_I
 
 let build_coq_False () = Lazy.force coq_False
-let build_coq_proof_admitted () = Lazy.force coq_proof_admitted
 let build_coq_not ()   = Lazy.force coq_not
 let build_coq_and ()   = Lazy.force coq_and
 let build_coq_conj ()  = Lazy.force coq_conj
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 986a4385..41204a71 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -160,7 +160,6 @@ val build_coq_sumbool : constr delayed
 (** Connectives 
    The False proposition *)
 val build_coq_False : constr delayed
-val build_coq_proof_admitted : constr delayed
 
 (** The True proposition and its unique proof *)
 val build_coq_True : constr delayed
diff --git a/interp/genintern.ml b/interp/genintern.ml
index c78b13a8..7795946d 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -12,7 +12,6 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   genv : Environ.env }
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 6e63f71c..28f4f530 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -12,7 +12,6 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   genv : Environ.env }
 
 (** {5 Internalization functions} *)
diff --git a/interp/modintern.ml b/interp/modintern.ml
index fdc6e609..bf0b2f98 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,7 +61,9 @@ let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
-      WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*)
+    let c, ectx = interp_constr env (Evd.from_env env) c in
+    let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in
+      WithDef (fqid,(c,ctx))
 
 let loc_of_module = function
   | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
diff --git a/interp/notation.ml b/interp/notation.ml
index aeec4b61..80db2cb3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -136,10 +136,6 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 (* Exportation of scopes *)
 let open_scope i (_,(local,op,sc)) =
   if Int.equal i 1 then
-    let sc = match sc with
-      | Scope sc -> Scope (normalize_scope sc)
-      | _ -> sc
-    in
     scope_stack :=
       if op then sc :: !scope_stack
       else List.except scope_eq sc !scope_stack
@@ -166,7 +162,7 @@ let inScope : bool * bool * scope_elem -> obj =
       classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
-  Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
+  Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc)))
 
 let empty_scope_stack = []
 
@@ -516,6 +512,32 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 (* Miscellaneous *)
 
+let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
+
+let ntpe_eq t1 t2 = match t1, t2 with
+| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeConstrList, NtnTypeConstrList -> true
+| NtnTypeBinderList, NtnTypeBinderList -> true
+| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+
+
+let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
+  Id.equal id1 id2 &&
+  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  ntpe_eq tp1 tp2
+
+let interpretation_eq (vars1, t1) (vars2, t2) =
+  List.equal vars_eq vars1 vars2 &&
+  Notation_ops.eq_notation_constr t1 t2
+
+let exists_notation_in_scope scopt ntn r =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = String.Map.find scope !scope_map in
+    let (r',_) = String.Map.find ntn sc.notations in
+    interpretation_eq r' r
+  with Not_found -> false
+
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
diff --git a/interp/notation.mli b/interp/notation.mli
index c66115cb..854c52b2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -140,6 +140,10 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
 
+(** Checks for already existing notations *)
+val exists_notation_in_scope : scope_name option -> notation ->
+      interpretation -> bool
+
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> global_reference -> scope_name option list -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c91c7815..2762dc0b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -170,6 +170,69 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
 
 let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
 
+let rec eq_notation_constr t1 t2 = match t1, t2 with
+| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NVar id1, NVar id2 -> Id.equal id1 id2
+| NApp (t1, a1), NApp (t2, a2) ->
+  eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2 && b1 == b2
+| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+  let eqpat (p1, t1) (p2, t2) =
+    List.equal cases_pattern_eq p1 p2 &&
+    eq_notation_constr t1 t2
+  in
+  let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
+    let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+    eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+  in
+  Option.equal eq_notation_constr o1 o2 &&
+  List.equal eqf r1 r2 &&
+  List.equal eqpat p1 p2
+| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+  List.equal Name.equal nas1 nas2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+  eq_notation_constr t1 t2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr u1 u2 &&
+  eq_notation_constr r1 r2
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+  let eq (na1, o1, t1) (na2, o2, t2) =
+    Name.equal na1 na2 &&
+    Option.equal eq_notation_constr o1 o2 &&
+    eq_notation_constr t1 t2
+  in
+  Array.equal Id.equal ids1 ids2 &&
+  Array.equal (List.equal eq) ts1 ts2 &&
+  Array.equal eq_notation_constr us1 us2 &&
+  Array.equal eq_notation_constr rs1 rs2
+| NSort s1, NSort s2 ->
+  Miscops.glob_sort_eq s1 s2
+| NPatVar p1, NPatVar p2 ->
+  Id.equal p1 p2
+| NCast (t1, c1), NCast (t2, c2) ->
+  eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+  | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+  | NRec _ | NSort _ | NPatVar _ | NCast _), _ -> false
+
+
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 7283ed6f..c6770dee 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -25,6 +25,8 @@ val ldots_var : Id.t
 (** FIXME: nothing to do here *)
 val eq_glob_constr : glob_constr -> glob_constr -> bool
 
+val eq_notation_constr : notation_constr -> notation_constr -> bool
+
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->