aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4cfa0a0da..51fcd9c07 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
@@ -24,12 +24,12 @@ open Mod_subst
(* non global expressions such as existential variables also *)
type aconstr =
- (* Part common to rawconstr and cases_pattern *)
+ (* Part common to [rawconstr] and [cases_pattern] *)
| ARef of global_reference
| AVar of identifier
| AApp of aconstr * aconstr list
| AList of identifier * identifier * aconstr * aconstr * bool
- (* Part only in rawconstr *)
+ (* Part only in [rawconstr] *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
@@ -60,7 +60,7 @@ type scope_name = string
type interpretation =
(identifier * (scope_name option * scope_name list)) list * aconstr
-val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
+val match_aconstr : rawconstr -> interpretation ->
(rawconstr * (scope_name option * scope_name list)) list
(*s Concrete syntax for terms *)