diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 22:30:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 22:30:44 +0000 |
| commit | 7944955b892f0ffa70ecf92f83b372cddc5b867b (patch) | |
| tree | 479fc9f009fa1a81490c016956c61d6f7c62896c /interp/constrintern.ml | |
| parent | 90e5407fcfc59dce5ea592aeae6195183a2b4ad2 (diff) | |
Modifications diverses et variées :
- Nouvel essai de prise en compte unfold dans apply (unification.ml)
- Correction bug commit précédent (constrintern.ml)
- Correction bug d'explication des evars non résolues (evarutil.ml)
- Fenêtre de query coqide plus large (command_windows.ml)
- Orthographe tauto (tauto.ml4)
- Crédits (ConstructiveEpsilon.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a0e9b6bb5..55f3d9fba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -606,7 +606,7 @@ let find_constructor ref f aliases pats scopes = let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in cstr, idspl1, pats2 - | _ -> error_invalid_pattern_notation loc) + | _ -> raise Not_found) | TrueGlobal r -> let rec unf = function |