From 6679d01256ce9a4a05c13eabbb4e2d85c3e6f075 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 21:08:39 +0000
Subject: Added new command "Set Parsing Explicit" for deactivating parsing
 (and printing) of implicit arguments (a priori useful for teaching).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7b0d4ff2b8..f36d56b83f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -166,6 +166,8 @@ let error_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
+let parsing_explicit = ref false
+
 let empty_internalization_env = Idmap.empty
 
 let compute_explicitable_implicit imps = function
@@ -1215,6 +1217,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CRef ref as x ->
 	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
+        assert (l=[]);
 	(match intern_impargs c env imp subscopes l with
            | [] -> c
            | l -> GApp (constr_loc x, c, l))
@@ -1333,7 +1336,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
                 find_appl_head_data c, args
             | x -> (intern env f,[],[],[]), args in
 	let args =
-	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
+          intern_impargs c env impargs args_scopes (merge_impargs l args) in
 	check_projection isproj (List.length args) c;
 	(match c with
           (* Now compact "(f args') args" *)
@@ -1490,6 +1493,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
   and intern_impargs c env l subscopes args =
     let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
+    if !parsing_explicit then
+      if eargs <> [] then
+        error "Arguments given by name or position not supported in explicit mode."
+      else
+        intern_args env subscopes rargs
+    else
     let rec aux n impl subscopes eargs rargs =
       let (enva,subscopes') = apply_scope_env env subscopes in
       match (impl,rargs) with
-- 
cgit v1.2.3