diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-26 20:30:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-26 20:30:29 +0000 |
| commit | 535790b58a83879bdabd61914f68efe8e1ec469a (patch) | |
| tree | 9dbf3f5145c31b60eb4f57c9ebfd5248fa67bfa2 /interp | |
| parent | fb119901df9d336886c69f558874ddc05c085fbb (diff) | |
Partial revert of r14292
No more assertion failure because of half done job.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14301 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 91e374f59..33dec8aa6 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 |