From cf69befd5678b6827126ef0a2b89218ea7b02c89 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 7 Jul 2008 14:14:08 +0000 Subject: - Improve [Context] vernacular to allow arbitrary binders, not just classes, and simplify the implementation. - Experimental syntax {{ cl : Class args }} and (( cl : Class args )) which respectively make cl an implicit or explicit argument ({{ }} is equivalent to [ ]). Could be extended to any type of binder, eg. [Definition flip ((R : relation carrier)) : relation carrier := ...]. The idea behind double brackets is to distinguish macro-binders which perform implicit generalization from regular binders. It could also save [ ] for other uses. - Fix bug #1901 about {} binders in records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11210 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/termops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/termops.mli') diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 539951d5c..15751b91c 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -185,7 +185,7 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr -(* Get the last arg of a constr intended to be nn application *) +(* Get the last arg of a constr intended to be an application *) val last_arg : constr -> constr (* name contexts *) -- cgit v1.2.3