diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /parsing/astterm.ml | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/astterm.ml')
| -rw-r--r-- | parsing/astterm.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index bfd4e6685..81fdc9229 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -156,7 +156,7 @@ let ids_of_ctxt ctxt = ctxt) type pattern_qualid_kind = - | IsConstrPat of loc * (constructor_path * identifier list) + | IsConstrPat of loc * constructor | IsVarPat of loc * identifier let maybe_constructor env = function @@ -164,8 +164,7 @@ let maybe_constructor env = function let qid = interp_qualid l in (try match kind_of_term (global_qualified_reference qid) with - | IsMutConstruct ((spi,j),cl) -> - IsConstrPat (loc,((spi,j),ids_of_ctxt cl)) + | IsMutConstruct c -> IsConstrPat (loc,c) | _ -> (match maybe_variable l with | Some s -> @@ -183,13 +182,13 @@ let maybe_constructor env = function (* This may happen in quotations *) | Node(loc,"MUTCONSTRUCT",[sp;Num(_,ti);Num(_,n)]) -> (* Buggy: needs to compute the context *) - IsConstrPat (loc,(((ast_to_sp sp,ti),n),[])) + IsConstrPat (loc,((ast_to_sp sp,ti),n)) | Path(loc,sp) -> (match absolute_reference sp with - | ConstructRef (spi,j) -> - IsConstrPat (loc,((spi,j),[])) - | _ -> error ("Unknown absolute constructor name: "^(string_of_path sp))) + | ConstructRef c -> IsConstrPat (loc,c) + | _ -> + error ("Unknown absolute constructor name: "^(string_of_path sp))) | Node(loc,("CONST"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) -> user_err_loc (loc,"ast_to_pattern", |