Merge branch 'v8.6'

3 files changed, 52 insertions, 22 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index dc5ce1a53..8e6a0f6a7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -386,7 +386,13 @@ let context poly l =
       let ctx = Univ.ContextSet.to_context !uctx in
       (* Declare the universe context once *)
       let () = uctx := Univ.ContextSet.empty in
-      let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
+      let decl = match b with
+      | None ->
+        (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+      | Some b ->
+        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        (DefinitionEntry entry, IsAssumption Logical)
+      in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr !evars (EConstr.of_constr t) with
 	| Some (rels, ((tc,_), args) as _cl) ->
@@ -402,9 +408,17 @@ let context poly l =
       in
       let impl = List.exists test impls in
       let decl = (Discharge, poly, Definitional) in
-      let nstatus =
+      let nstatus = match b with
+      | None ->
         pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
           Vernacexpr.NoInline (Loc.tag id))
+      | Some b ->
+        let ctx = Univ.ContextSet.to_context !uctx in
+        let decl = (Discharge, poly, Definition) in
+        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+        let _ = Command.declare_definition id decl entry [] [] hook in
+        Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
       let () = uctx := Univ.ContextSet.empty in
 	status && nstatus
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 34b9b97d8..a114553cd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -301,22 +301,22 @@ let is_numeral symbs =
   | _ ->
       false
 
-let rec get_notation_vars = function
+let rec get_notation_vars onlyprint = function
   | [] -> []
   | NonTerminal id :: sl ->
-      let vars = get_notation_vars sl in
+      let vars = get_notation_vars onlyprint sl in
       if Id.equal id ldots_var then vars else
-	if Id.List.mem id vars then
+	(* don't check for nonlinearity if printing only, see Bug 5526 *)
+	if not onlyprint && Id.List.mem id vars then 
 	  user_err ~hdr:"Metasyntax.get_notation_vars"
             (str "Variable " ++ pr_id id ++ str " occurs more than once.")
-	else
-          id::vars
-  | (Terminal _ | Break _) :: sl -> get_notation_vars sl
+	else id::vars
+  | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
   | SProdList _ :: _ -> assert false
 
-let analyze_notation_tokens l =
+let analyze_notation_tokens ~onlyprint l =
   let l = raw_analyze_notation_tokens l in
-  let vars = get_notation_vars l in
+  let vars = get_notation_vars onlyprint l in
   let recvars,l = interp_list_parser [] l in
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
@@ -1084,12 +1084,12 @@ let compute_syntax_data df modifiers =
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some NonA) in
   let toks = split_notation_string df in
-  let recvars,mainvars,symbols = analyze_notation_tokens toks in
+  let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint toks in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
   let _ = check_binder_type recvars mods.etyps in
 
   (* Notations for interp and grammar  *)
-let ntn_for_interp = make_notation_key symbols in
+  let ntn_for_interp = make_notation_key symbols in
   let symbols' = remove_curly_brackets symbols in
   let ntn_for_grammar = make_notation_key symbols' in
   if not onlyprint then check_rule_productivity symbols';
@@ -1333,7 +1333,7 @@ let add_notation_in_scope local df c mods scope =
 
 let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
   let dfs = split_notation_string df in
-  let recvars,mainvars,symbs = analyze_notation_tokens dfs in
+  let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let i_typs, onlyprint = if not (is_numeral symbs) then begin
     let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
@@ -1410,7 +1410,7 @@ let add_notation local c ((loc,df),modifiers) sc =
 let add_notation_extra_printing_rule df k v =
   let notk = 
     let dfs = split_notation_string df in
-    let _,_, symbs = analyze_notation_tokens dfs in
+    let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in
     make_notation_key symbs in
   Notation.add_notation_extra_printing_rule notk k v
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 69492759b..ef16df5b7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -108,14 +108,29 @@ let show_intro all =
     [Not_found] is raised if the given string isn't the qualid of
     a known inductive type. *)
 
+(*
+
+  HH notes in PR #679:
+
+  The Show Match could also be made more robust, for instance in the
+  presence of let in the branch of a constructor. A
+  decompose_prod_assum would probably suffice for that, but then, it
+  is a Context.Rel.Declaration.t which needs to be matched and not
+  just a pair (name,type).
+
+  Otherwise, this is OK. After all, the API on inductive types is not
+  so canonical in general, and in this simple case, working at the
+  low-level of mind_nf_lc seems reasonable (compared to working at the
+  higher-level of Inductiveops).
+
+*)
+    
 let make_cases_aux glob_ref =
   match glob_ref with
-    | Globnames.IndRef i ->
-	let {Declarations.mind_nparams = np}
-	    , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
-	      = Global.lookup_inductive i in
-	Util.Array.fold_right2
-	  (fun consname typ l ->
+    | Globnames.IndRef ind ->
+	let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+	Util.Array.fold_right_i
+	  (fun i typ l ->
 	     let al = List.rev (fst (decompose_prod typ)) in
 	     let al = Util.List.skipn np al in
 	     let rec rename avoid = function
@@ -124,8 +139,9 @@ let make_cases_aux glob_ref =
 		   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
 		   Id.to_string n' :: rename (n'::avoid) l in
 	     let al' = rename [] al in
-	     (Id.to_string consname :: al') :: l)
-	  carr tarr []
+	     let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
+	     (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
+	  tarr []
     | _ -> raise Not_found
 
 let make_cases s =