diff options
| author | herbelin | 2000-01-26 17:22:13 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-26 17:22:13 +0000 |
| commit | d56cc2ca71eee52a26f401ad2b37b8d9e6019a3c (patch) | |
| tree | 989cc0c825d7c8ac2e95e5f173caf24ae3cd29f7 /tactics/pattern.ml | |
| parent | 3c0c85ea71400cd4b2d1dc5630405dc1f90aa5f3 (diff) | |
MAJ ocaml 2.99 (espaces dans la syntaxe des cast)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@284 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/pattern.ml')
| -rw-r--r-- | tactics/pattern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 239b5e84f3..78fa139741 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -82,13 +82,13 @@ let dest_soapp_operator = function Some (n,list_uniquize [p]) | _ -> None -let constrain ((n:int),(m:constr)) sigma = +let constrain ((n : int),(m : constr)) sigma = if List.mem_assoc n sigma then if eq_constr m (List.assoc n sigma) then sigma else error "somatch" else (n,m)::sigma -let build_dlam toabstract stk (m:constr) = +let build_dlam toabstract stk (m : constr) = let rec buildrec m p_0 p_1 = match p_0,p_1 with | (_, []) -> m | (n, (na::tl)) -> |