From 36c448f43c7fa16163b543b941be4a917a712a37 Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 27 Oct 2009 19:43:51 +0000 Subject: Add a new vernacular command for controling implicit generalization of variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/implicit_quantifiers.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'interp/implicit_quantifiers.mli') diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 0d28eccad..8f02eb765 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -24,6 +24,8 @@ open Libnames open Typeclasses (*i*) +val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit + val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list -- cgit v1.2.3