diff options
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 13 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 2 |
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" |