diff options
| -rw-r--r-- | interp/constrextern.ml | 4 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 1 |
2 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 91e374f59b..33dec8aa69 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -319,7 +319,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) = let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) - if l = [] then CPatAtom (loc,Some qid) else CPatCstrExpl (loc,qid,l) + if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l) (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = @@ -361,7 +361,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = CPatRecord(loc, List.rev (ip projs args [])) with Not_found | No_match | Exit -> - CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), args) in + CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) in insert_pat_alias loc p na and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 811f170dc8..940e14554b 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -178,7 +178,6 @@ let rec pr_patt sep inh p = | CPatCstr (_,c,args) -> pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp | CPatCstrExpl (_,c,args) -> - assert (args <> []); str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp | CPatAtom (_,None) -> str "_", latom | CPatAtom (_,Some r) -> pr_reference r, latom |