Little fixes: print unbound variable in error message (patch by Samuel

Bronson), some keywords in coqdoc, and test well-typedness of predicate 
in subtac_cases after abstraction.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 15 insertions, 5 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 8312c66da8..c1b1283c63 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1979,7 +1979,7 @@ let nf_evars_env evar_defs (env : env) : env =
       
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let prepare_predicate_from_arsign_tycon loc env tomatchs arsign c =
+let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
   let subst, len = 
     List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
@@ -2016,7 +2016,13 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs arsign c =
 	      mkRel (n + nar))
       | _ ->
 	  map_constr_with_binders succ predicate lift c 
-  in predicate 0 c
+  in
+    try 
+      (* The tycon may be ill-typed after abstraction. *)
+      let pred = predicate 0 c in
+      let env' = push_rel_context (context_of_arsign arsign) env in
+	ignore(Typing.sort_of env' evm pred); pred
+    with _ -> lift nar c
 
 let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
 
@@ -2047,7 +2053,8 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	match valcon_of_tycon tycon with
 	| None -> let ev = mkExistential env isevars in ev, ev
 	| Some t -> 
-	    t, prepare_predicate_from_arsign_tycon loc env tomatchs sign (lift tomatchs_len t)
+	    t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
+	      tomatchs sign (lift tomatchs_len t)
       in
       let arity = 
 	it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8b0632c199..876f13c33d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1210,7 +1210,8 @@ let coerce_to_int = function
 
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
-  with Not_found -> user_err_loc(fst locid,"interp_int",str "Unbound variable")
+  with Not_found -> user_err_loc(fst locid,"interp_int",
+				str "Unbound variable"  ++ pr_id (snd locid))
 
 let interp_int_or_var ist = function
   | ArgVar locid -> interp_int ist locid
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 067af63f2b..0522bbac08 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -42,7 +42,7 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Set"; "Unset"; "Variable"; "Variables"; 
+      "Set"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; 
       "Boxed"; "Unboxed"; "Inline";
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 36ed0472b2..d78aabbf93 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -246,6 +247,7 @@ let gallina_ext =
   | "Tactic" space+ "Notation"
   | "Reserved" space+ "Notation"
   | "Section"
+  | "Context"
   | "Variable" 's'?
   | ("Hypothesis" | "Hypotheses")
   | "End"